Forgetting a specific belief revision episode may not erase information because the other revisions may provide or entail the same information. Whether it does was proved coNP-hard for sequences of two arbitrary lexicographic revisions or arbitrarily long lexicographic Horn revisions. A polynomial algorithm is presented for the case of two lexicographic Horn revision. Heterogeneous sequences, including revisions other than lexicographic, were proved to belong in Delta2. Their previously proved coNP-hardness is enhanced to Dp-hardness.

We investigate an approach for extracting knowledge from trained neural networks based on Angluin's exact learning model with membership and equivalence queries to an oracle. In this approach, the oracle is a trained neural network. We consider Angluin's classical algorithm for learning Horn theories and study the necessary changes to make it applicable to learn from neural networks. In particular, we have to consider that trained neural networks may not behave as Horn oracles, meaning that their underlying target theory may not be Horn. We propose a new algorithm that aims at extracting the "tightest Horn approximation" of the target theory and that is guaranteed to terminate in exponential time (in the worst case) and in polynomial time if the target has polynomially many non-Horn examples. To showcase the applicability of the approach, we perform experiments on pre-trained language models and extract rules that expose occupation-based gender biases.

The expressiveness of propositional non-clausal (NC) formulas is exponentially richer than that of clausal formulas. Yet, clausal efficiency outperforms non-clausal one. Indeed, a major weakness of the latter is that, while Horn clausal formulas, along with Horn algorithms, are crucial for the high efficiency of clausal reasoning, no Horn-like formulas in non-clausal form had been proposed. To overcome such weakness, we define the hybrid class $\mathbb{H_{NC}}$ of Horn Non-Clausal (Horn-NC) formulas, by adequately lifting the Horn pattern to NC form, and argue that $\mathbb{H_{NC}}$, along with future Horn-NC algorithms, shall increase non-clausal efficiency just as the Horn class has increased clausal efficiency. Secondly, we: (i) give the compact, inductive definition of $\mathbb{H_{NC}}$; (ii) prove that syntactically $\mathbb{H_{NC}}$ subsumes the Horn class but semantically both classes are equivalent, and (iii) characterize the non-clausal formulas belonging to $\mathbb{H_{NC}}$. Thirdly, we define the Non-Clausal Unit-Resolution calculus, $UR_{NC}$, and prove that it checks the satisfiability of $\mathbb{H_{NC}}$ in polynomial time. This fact, to our knowledge, makes $\mathbb{H_{NC}}$ the first characterized polynomial class in NC reasoning. Finally, we prove that $\mathbb{H_{NC}}$ is linearly recognizable, and also that it is both strictly succincter and exponentially richer than the Horn class. We discuss that in NC automated reasoning, e.g. satisfiability solving, theorem proving, logic programming, etc., can directly benefit from $\mathbb{H_{NC}}$ and $UR_{NC}$ and that, as a by-product of its proved properties, $\mathbb{H_{NC}}$ arises as a new alternative to analyze Horn functions and implication systems.

In this paper we investigate CNF formulas, for which the unit propagation is strong enough to derive a contradiction if the formula together with a partial assignment of the variables is unsatisfiable (unit refutation complete or URC formulas) or additionally to derive all implied literals if the formula is satisfiable (propagation complete or PC formulas). If a formula represents a function using existentially quantified auxiliary variables, it is called an encoding of the function. We prove several results on the sizes of PC and URC formulas and encodings. One of them are separations between the sizes of formulas of different types. Namely, we prove an exponential separation between the size of URC formulas and PC formulas and between the size of PC encodings using auxiliary variables and URC formulas. Besides of this, we prove that the sizes of any two irredundant PC formulas for the same function differ at most by a polynomial factor in the number of the variables and present an example of a function demonstrating that a similar statement is not true for URC formulas. One of the separations above implies that a q-Horn formula may require an exponential number of additional clauses to become a URC formula. On the other hand, for every q-Horn formula, we present a polynomial size URC encoding of the same function using auxiliary variables. This encoding is not q-Horn in general.

We describe a compilation language of backdoor decomposable monotone circuits (BDMCs) which generalizes several concepts appearing in the literature, e.g. DNNFs and backdoor trees. A BDMC sentence is a monotone circuit which satisfies decomposability property (such as in DNNF) in which the inputs (or leaves) are associated with CNF encodings of some functions. We consider two versions of BDMCs. In case of PC-BDMCs the encodings in the leaves are propagation complete encodings and in case of URC-BDMCs the encodings in the leaves are unit refutation complete encodings of respective functions. We show that a representation of a boolean function with a PC-BDMC can be transformed into a propagation complete encoding of the same function whose size is polynomial in the size of the input PC-BDMC sentence. We obtain a similar result in case of URC-BDMCs. We also relate the size of PC-BDMCs to the size of DNNFs and backdoor trees.

Judgment aggregation is a general framework for collective decision making that can be used to model many different settings. Due to its general nature, the worst case complexity of essentially all relevant problems in this framework is very high. However, these intractability results are mainly due to the fact that the language to represent the aggregation domain is overly expressive. We initiate an investigation of representation languages for judgment aggregation that strike a balance between (1) being limited enough to yield computational tractability results and (2) being expressive enough to model relevant applications. In particular, we consider the languages of Krom formulas, (definite) Horn formulas, and Boolean circuits in decomposable negation normal form (DNNF). We illustrate the use of the positive complexity results that we obtain for these languages with a concrete application: voting on how to spend a budget (i.e., participatory budgeting).

We propose an algorithm for learning the Horn envelope of an arbitrary domain using an expert, or an oracle, capable of answering certain types of queries about this domain. Attribute exploration from formal concept analysis is a procedure that solves this problem, but the number of queries it may ask is exponential in the size of the resulting Horn formula in the worst case. We recall a well-known polynomial-time algorithm for learning Horn formulas with membership and equivalence queries and modify it to obtain a polynomial-time probably approximately correct algorithm for learning the Horn envelope of an arbitrary domain. Keywords: PAC learning, attribute exploration, FCA, formal concept 2010 MSC: 68T27, 06B99 1. Introduction The learnability of concepts from oracle queries has received significant attention in learning theory. The most common types of oracles investigated in the literature are membership and equivalence oracles, and for these types of oracles various results have been obtained showing learnability in polynomial time. One of the most prominent examples is the fact that Horn formulas can be learnt in polynomial time with access to membership and equivalence oracles [1]. In the realm of formal concept analysis [2], a different learning method has been established almost simultaneously with the standard query learning setting. The theory of formal concept analysis emerged as a subfield of mathematical order theory, more precisely of lattice theory, and it studies lattices as hierarchies of concepts. Since its emergence in the early 1980s, it has evolved into a rich theory with a wide range of applications. An important technique of formal concept analysis is the attribute exploration algorithm. A Horn envelope of a theory is a Horn formula whose set of models includes all the models of the theory and is as specific as possible [3].

The plans that planning systems generate for solvable planning tasks are routinely verified by independent validation tools. For unsolvable planning tasks, no such validation capabilities currently exist. We describe a family of certificates of unsolvability for classical planning tasks that can be efficiently verified and are sufficiently general for a wide range of planning approaches including heuristic search with delete relaxation, critical-path, pattern database and linear merge-and-shrink heuristics, symbolic search with binary decision diagrams, and the Trapper algorithm for detecting dead ends. We also augmented a classical planning system with the ability to emit certificates of unsolvability and implemented a planner-independent certificate validation tool. Experiments show that the overhead for producing such certificates is tolerable and that their validation is practically feasible.

Belief merging is a central operation within the field of belief change and addresses the problem of combining multiple, possibly mutually inconsistent knowledge bases into a single, consistent one. A current research trend in belief change is concerned with tailored representation theorems for fragments of logic, in particular Horn logic. Hereby, the goal is to guarantee that the result of the change operations stays within the fragment under consideration. While several such results have been obtained for Horn revision and Horn contraction, merging of Horn theories has been neglected so far. In this paper, we provide a novel representation theorem for Horn merging by strengthening the standard merging postulates. Moreover, we present a concrete Horn merging operator satisfying all postulates.

The AGM framework is the benchmark approach in belief change. Since the framework assumes an underlying logic containing classical Propositional Logic, it can not be applied to systems with a logic weaker than Propositional Logic. To remedy this limitation, several researchers have studied AGM-style contraction and revision under the Horn fragment of Propositional Logic (i.e., Horn logic). In this paper, we contribute to this line of research by investigating the Horn version of the AGM entrenchment-based contraction. The study is challenging as the construction of entrenchment-based contraction refers to arbitrary disjunctions which are not expressible under Horn logic. In order to adapt the construction to Horn logic, we make use of a Horn approximation technique called Horn strengthening. We provide a representation theorem for the newly constructed contraction which we refer to as entrenchment-based Horn contraction. Ideally, contractions defined under Horn logic (i.e., Horn contractions) should be as rational as AGM contraction. We propose the notion of Horn equivalence which intuitively captures the equivalence between Horn contraction and AGM contraction. We show that, under this notion, entrenchment-based Horn contraction is equivalent to a restricted form of entrenchment-based contraction.